package tests;

import base.Atome;
import base.Formule;
import operateurs.Et;
import operateurs.Implique;
import operateurs.Non;
import operateurs.Ou;
import preuve.Preuve;
import quantifieurs.PourTout;
import termes.Variable;

public class Application {
	public static void main(String[] args) {

		/*
		 * Preuve à effectuer
		- les bébés sont illogiques
		- nul n'est méprisé quand il peut venir à bout d'un crocodile
		- les gens illogiques sont méprisés 
		- donc : les bébés ne peuvent venir à bout des crocodiles
		 */

		Formule premisses = new Et(new PourTout(new Variable("x"), new Implique(new Atome("bebe", new Variable("x")), new Atome("illogique", new Variable("x")))),
				new Et( new PourTout(new Variable("x"), new Implique(new Atome("crocodile", new Variable("x")), new Non(new Atome("meprise", new Variable("x"))))),
						new PourTout(new Variable("x"), new Implique(new Atome("illogique", new Variable("x")), new Atome("meprise", new Variable("x"))))
						));

		Formule conclusion = new PourTout(new Variable("x"), new Implique(new Atome("bebe", new Variable("x")), new Non(new Atome("crocodile", new Variable("x")))));

		Preuve preuve = new Preuve(premisses, conclusion);
		preuve.doPreuve();
	}
}